Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
2 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
3 | 1, 2 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐โ๐) ยท (๐โ๐)) = ((๐โ๐) ยท (๐โ๐))) |
4 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
5 | 4 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) = (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) |
6 | 3, 5 | breq12d 5119 |
. . . . . . . . 9
โข (๐ = ๐ โ (((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)))) |
7 | 6 | cbvralvw 3224 |
. . . . . . . 8
โข
(โ๐ โ
โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) |
8 | | nnre 12165 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
9 | | 1re 11160 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
10 | | lelttric 11267 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โค 1
โจ 1 < ๐)) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โค 1 โจ 1 < ๐)) |
12 | 11 | ancli 550 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ โ โ โง (๐ โค 1 โจ 1 < ๐))) |
13 | | andi 1007 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โค 1 โจ 1 < ๐)) โ ((๐ โ โ โง ๐ โค 1) โจ (๐ โ โ โง 1 < ๐))) |
14 | 12, 13 | sylib 217 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((๐ โ โ โง ๐ โค 1) โจ (๐ โ โ โง 1 <
๐))) |
15 | | nnge1 12186 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 1 โค
๐) |
16 | | letri3 11245 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง 1 โ
โ) โ (๐ = 1
โ (๐ โค 1 โง 1
โค ๐))) |
17 | 8, 9, 16 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (๐ = 1 โ (๐ โค 1 โง 1 โค ๐))) |
18 | 17 | biimpar 479 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ โค 1 โง 1 โค ๐)) โ ๐ = 1) |
19 | 18 | anassrs 469 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ โค 1) โง 1 โค ๐) โ ๐ = 1) |
20 | 15, 19 | mpidan 688 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โค 1) โ ๐ = 1) |
21 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (๐ โ 1) = (1 โ 1)) |
22 | | 1m1e0 12230 |
. . . . . . . . . . . . . . . 16
โข (1
โ 1) = 0 |
23 | 21, 22 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ (๐ โ 1) = 0) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โค 1) โ (๐ โ 1) =
0) |
25 | | faclbnd4lem3 14201 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐ โ 1) = 0) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1)))) |
26 | 24, 25 | sylan2 594 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐ โ โ โง ๐ โค 1)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1)))) |
27 | 26 | a1d 25 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐ โ โ โง ๐ โค 1)) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
28 | | 1nn 12169 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
29 | | nnsub 12202 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ๐
โ โ) โ (1 < ๐ โ (๐ โ 1) โ โ)) |
30 | 28, 29 | mpan 689 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (1 <
๐ โ (๐ โ 1) โ
โ)) |
31 | 30 | biimpa 478 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง 1 <
๐) โ (๐ โ 1) โ
โ) |
32 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ 1) โ (๐โ๐) = ((๐ โ 1)โ๐)) |
33 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ 1) โ (๐โ๐) = (๐โ(๐ โ 1))) |
34 | 32, 33 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ โ 1) โ ((๐โ๐) ยท (๐โ๐)) = (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1)))) |
35 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ 1) โ (!โ๐) = (!โ(๐ โ 1))) |
36 | 35 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ โ 1) โ (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) = (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1)))) |
37 | 34, 36 | breq12d 5119 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ โ 1) โ (((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
38 | 37 | rspcv 3576 |
. . . . . . . . . . . . . 14
โข ((๐ โ 1) โ โ
โ (โ๐ โ
โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
39 | 31, 38 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 1 <
๐) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
40 | 39 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ
โ0) โง (๐ โ โ โง 1 < ๐)) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
41 | 27, 40 | jaodan 957 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((๐ โ โ โง ๐ โค 1) โจ (๐ โ โ โง 1 < ๐))) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
42 | 14, 41 | sylan2 594 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ๐ โ โ) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ (((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))))) |
43 | | faclbnd4lem2 14200 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0 โง ๐
โ โ) โ ((((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
44 | 43 | 3expa 1119 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ๐ โ โ) โ ((((๐ โ 1)โ๐) ยท (๐โ(๐ โ 1))) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
45 | 42, 44 | syld 47 |
. . . . . . . . 9
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ๐ โ โ) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
46 | 45 | ralrimdva 3148 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
47 | 7, 46 | biimtrid 241 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
48 | 47 | expcom 415 |
. . . . . 6
โข (๐ โ โ0
โ (๐ โ
โ0 โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐))))) |
49 | 48 | a2d 29 |
. . . . 5
โข (๐ โ โ0
โ ((๐ โ
โ0 โ โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) โ (๐ โ โ0 โ
โ๐ โ โ
((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐))))) |
50 | | nnnn0 12425 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ0) |
51 | | faclbnd3 14198 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) |
52 | 50, 51 | sylan2 594 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) |
53 | | nncn 12166 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
54 | 53 | exp0d 14051 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐โ0) = 1) |
55 | 54 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐โ0) ยท (๐โ๐)) = (1 ยท (๐โ๐))) |
56 | 55 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐โ0) ยท
(๐โ๐)) = (1 ยท (๐โ๐))) |
57 | | nn0cn 12428 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ๐ โ
โ) |
58 | | expcl 13991 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
59 | 57, 50, 58 | syl2an 597 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐โ๐) โ
โ) |
60 | 59 | mulid2d 11178 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (1 ยท (๐โ๐)) = (๐โ๐)) |
61 | 56, 60 | eqtrd 2773 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐โ0) ยท
(๐โ๐)) = (๐โ๐)) |
62 | | sq0 14102 |
. . . . . . . . . . . . . 14
โข
(0โ2) = 0 |
63 | 62 | oveq2i 7369 |
. . . . . . . . . . . . 13
โข
(2โ(0โ2)) = (2โ0) |
64 | | 2cn 12233 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
65 | | exp0 13977 |
. . . . . . . . . . . . . 14
โข (2 โ
โ โ (2โ0) = 1) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(2โ0) = 1 |
67 | 63, 66 | eqtri 2761 |
. . . . . . . . . . . 12
โข
(2โ(0โ2)) = 1 |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (2โ(0โ2)) = 1) |
69 | 57 | addid1d 11360 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ (๐ + 0) = ๐) |
70 | 69 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐โ(๐ + 0)) = (๐โ๐)) |
71 | 68, 70 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((2โ(0โ2)) ยท (๐โ(๐ + 0))) = (1 ยท (๐โ๐))) |
72 | | expcl 13991 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
73 | 57, 72 | mpancom 687 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐โ๐) โ
โ) |
74 | 73 | mulid2d 11178 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (1 ยท (๐โ๐)) = (๐โ๐)) |
75 | 71, 74 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((2โ(0โ2)) ยท (๐โ(๐ + 0))) = (๐โ๐)) |
76 | 75 | oveq1d 7373 |
. . . . . . . 8
โข (๐ โ โ0
โ (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐)) = ((๐โ๐) ยท (!โ๐))) |
77 | 76 | adantr 482 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐)) = ((๐โ๐) ยท (!โ๐))) |
78 | 52, 61, 77 | 3brtr4d 5138 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐โ0) ยท
(๐โ๐)) โค (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐))) |
79 | 78 | ralrimiva 3140 |
. . . . 5
โข (๐ โ โ0
โ โ๐ โ
โ ((๐โ0)
ยท (๐โ๐)) โค (((2โ(0โ2))
ยท (๐โ(๐ + 0))) ยท (!โ๐))) |
80 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = 0 โ (๐โ๐) = (๐โ0)) |
81 | 80 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = 0 โ ((๐โ๐) ยท (๐โ๐)) = ((๐โ0) ยท (๐โ๐))) |
82 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐โ2) = (0โ2)) |
83 | 82 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = 0 โ (2โ(๐โ2)) =
(2โ(0โ2))) |
84 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐ + ๐) = (๐ + 0)) |
85 | 84 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = 0 โ (๐โ(๐ + ๐)) = (๐โ(๐ + 0))) |
86 | 83, 85 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = 0 โ ((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) = ((2โ(0โ2)) ยท (๐โ(๐ + 0)))) |
87 | 86 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = 0 โ (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) = (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐))) |
88 | 81, 87 | breq12d 5119 |
. . . . . . 7
โข (๐ = 0 โ (((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ ((๐โ0) ยท (๐โ๐)) โค (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐)))) |
89 | 88 | ralbidv 3171 |
. . . . . 6
โข (๐ = 0 โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ0) ยท (๐โ๐)) โค (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐)))) |
90 | 89 | imbi2d 341 |
. . . . 5
โข (๐ = 0 โ ((๐ โ โ0 โ
โ๐ โ โ
((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) โ (๐ โ โ0 โ
โ๐ โ โ
((๐โ0) ยท (๐โ๐)) โค (((2โ(0โ2)) ยท (๐โ(๐ + 0))) ยท (!โ๐))))) |
91 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
92 | 91 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐โ๐) ยท (๐โ๐)) = ((๐โ๐) ยท (๐โ๐))) |
93 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
94 | 93 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (2โ(๐โ2)) = (2โ(๐โ2))) |
95 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
96 | 95 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ(๐ + ๐)) = (๐โ(๐ + ๐))) |
97 | 94, 96 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ ((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) = ((2โ(๐โ2)) ยท (๐โ(๐ + ๐)))) |
98 | 97 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) = (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) |
99 | 92, 98 | breq12d 5119 |
. . . . . . 7
โข (๐ = ๐ โ (((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)))) |
100 | 99 | ralbidv 3171 |
. . . . . 6
โข (๐ = ๐ โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)))) |
101 | 100 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ ((๐ โ โ0 โ
โ๐ โ โ
((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) โ (๐ โ โ0 โ
โ๐ โ โ
((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))))) |
102 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ (๐โ๐) = (๐โ(๐ + 1))) |
103 | 102 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ ((๐โ๐) ยท (๐โ๐)) = ((๐โ(๐ + 1)) ยท (๐โ๐))) |
104 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐โ2) = ((๐ + 1)โ2)) |
105 | 104 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (2โ(๐โ2)) = (2โ((๐ + 1)โ2))) |
106 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = (๐ + 1) โ (๐ + ๐) = (๐ + (๐ + 1))) |
107 | 106 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ (๐โ(๐ + ๐)) = (๐โ(๐ + (๐ + 1)))) |
108 | 105, 107 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ ((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) = ((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1))))) |
109 | 108 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) = (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐))) |
110 | 103, 109 | breq12d 5119 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
111 | 110 | ralbidv 3171 |
. . . . . 6
โข (๐ = (๐ + 1) โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐)))) |
112 | 111 | imbi2d 341 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ โ โ0 โ
โ๐ โ โ
((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) โ (๐ โ โ0 โ
โ๐ โ โ
((๐โ(๐ + 1)) ยท (๐โ๐)) โค (((2โ((๐ + 1)โ2)) ยท (๐โ(๐ + (๐ + 1)))) ยท (!โ๐))))) |
113 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐พ โ (๐โ๐) = (๐โ๐พ)) |
114 | 113 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐พ โ ((๐โ๐) ยท (๐โ๐)) = ((๐โ๐พ) ยท (๐โ๐))) |
115 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = ๐พ โ (๐โ2) = (๐พโ2)) |
116 | 115 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐พ โ (2โ(๐โ2)) = (2โ(๐พโ2))) |
117 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐พ โ (๐ + ๐) = (๐ + ๐พ)) |
118 | 117 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐พ โ (๐โ(๐ + ๐)) = (๐โ(๐ + ๐พ))) |
119 | 116, 118 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐พ โ ((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) = ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) |
120 | 119 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐พ โ (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) = (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
121 | 114, 120 | breq12d 5119 |
. . . . . . 7
โข (๐ = ๐พ โ (((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
122 | 121 | ralbidv 3171 |
. . . . . 6
โข (๐ = ๐พ โ (โ๐ โ โ ((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐)) โ โ๐ โ โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
123 | 122 | imbi2d 341 |
. . . . 5
โข (๐ = ๐พ โ ((๐ โ โ0 โ
โ๐ โ โ
((๐โ๐) ยท (๐โ๐)) โค (((2โ(๐โ2)) ยท (๐โ(๐ + ๐))) ยท (!โ๐))) โ (๐ โ โ0 โ
โ๐ โ โ
((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))))) |
124 | 49, 79, 90, 101, 112, 123 | nn0indALT 12604 |
. . . 4
โข (๐พ โ โ0
โ (๐ โ
โ0 โ โ๐ โ โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
125 | 124 | imp 408 |
. . 3
โข ((๐พ โ โ0
โง ๐ โ
โ0) โ โ๐ โ โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
126 | | oveq1 7365 |
. . . . . 6
โข (๐ = ๐ โ (๐โ๐พ) = (๐โ๐พ)) |
127 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
128 | 126, 127 | oveq12d 7376 |
. . . . 5
โข (๐ = ๐ โ ((๐โ๐พ) ยท (๐โ๐)) = ((๐โ๐พ) ยท (๐โ๐))) |
129 | | fveq2 6843 |
. . . . . 6
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
130 | 129 | oveq2d 7374 |
. . . . 5
โข (๐ = ๐ โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) = (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
131 | 128, 130 | breq12d 5119 |
. . . 4
โข (๐ = ๐ โ (((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐)))) |
132 | 131 | rspcva 3578 |
. . 3
โข ((๐ โ โ โง
โ๐ โ โ
((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
133 | 125, 132 | sylan2 594 |
. 2
โข ((๐ โ โ โง (๐พ โ โ0
โง ๐ โ
โ0)) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |
134 | 133 | 3impb 1116 |
1
โข ((๐ โ โ โง ๐พ โ โ0
โง ๐ โ
โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) |