Step | Hyp | Ref
| Expression |
1 | | oveq2 7416 |
. . . 4
โข (๐ = 0 โ ((๐ + 1)โ๐) = ((๐ + 1)โ0)) |
2 | 1 | oveq2d 7424 |
. . 3
โข (๐ = 0 โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ0))) |
3 | | oveq2 7416 |
. . . 4
โข (๐ = 0 โ (๐ + ๐) = (๐ + 0)) |
4 | 3 | fveq2d 6895 |
. . 3
โข (๐ = 0 โ (!โ(๐ + ๐)) = (!โ(๐ + 0))) |
5 | 2, 4 | breq12d 5161 |
. 2
โข (๐ = 0 โ (((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)) โ ((!โ๐) ยท ((๐ + 1)โ0)) โค (!โ(๐ + 0)))) |
6 | | oveq2 7416 |
. . . 4
โข (๐ = ๐ โ ((๐ + 1)โ๐) = ((๐ + 1)โ๐)) |
7 | 6 | oveq2d 7424 |
. . 3
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ๐))) |
8 | | oveq2 7416 |
. . . 4
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
9 | 8 | fveq2d 6895 |
. . 3
โข (๐ = ๐ โ (!โ(๐ + ๐)) = (!โ(๐ + ๐))) |
10 | 7, 9 | breq12d 5161 |
. 2
โข (๐ = ๐ โ (((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)) โ ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)))) |
11 | | oveq2 7416 |
. . . 4
โข (๐ = (๐ + 1) โ ((๐ + 1)โ๐) = ((๐ + 1)โ(๐ + 1))) |
12 | 11 | oveq2d 7424 |
. . 3
โข (๐ = (๐ + 1) โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ(๐ + 1)))) |
13 | | oveq2 7416 |
. . . 4
โข (๐ = (๐ + 1) โ (๐ + ๐) = (๐ + (๐ + 1))) |
14 | 13 | fveq2d 6895 |
. . 3
โข (๐ = (๐ + 1) โ (!โ(๐ + ๐)) = (!โ(๐ + (๐ + 1)))) |
15 | 12, 14 | breq12d 5161 |
. 2
โข (๐ = (๐ + 1) โ (((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)) โ ((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) โค (!โ(๐ + (๐ + 1))))) |
16 | | oveq2 7416 |
. . . 4
โข (๐ = ๐ โ ((๐ + 1)โ๐) = ((๐ + 1)โ๐)) |
17 | 16 | oveq2d 7424 |
. . 3
โข (๐ = ๐ โ ((!โ๐) ยท ((๐ + 1)โ๐)) = ((!โ๐) ยท ((๐ + 1)โ๐))) |
18 | | oveq2 7416 |
. . . 4
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
19 | 18 | fveq2d 6895 |
. . 3
โข (๐ = ๐ โ (!โ(๐ + ๐)) = (!โ(๐ + ๐))) |
20 | 17, 19 | breq12d 5161 |
. 2
โข (๐ = ๐ โ (((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)) โ ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)))) |
21 | | faccl 14242 |
. . . . 5
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
22 | 21 | nnred 12226 |
. . . 4
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
23 | 22 | leidd 11779 |
. . 3
โข (๐ โ โ0
โ (!โ๐) โค
(!โ๐)) |
24 | | nn0cn 12481 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ) |
25 | | peano2cn 11385 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ) |
26 | 24, 25 | syl 17 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
27 | 26 | exp0d 14104 |
. . . . 5
โข (๐ โ โ0
โ ((๐ + 1)โ0) =
1) |
28 | 27 | oveq2d 7424 |
. . . 4
โข (๐ โ โ0
โ ((!โ๐)
ยท ((๐ + 1)โ0))
= ((!โ๐) ยท
1)) |
29 | 21 | nncnd 12227 |
. . . . 5
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
30 | 29 | mulridd 11230 |
. . . 4
โข (๐ โ โ0
โ ((!โ๐)
ยท 1) = (!โ๐)) |
31 | 28, 30 | eqtrd 2772 |
. . 3
โข (๐ โ โ0
โ ((!โ๐)
ยท ((๐ + 1)โ0))
= (!โ๐)) |
32 | 24 | addridd 11413 |
. . . 4
โข (๐ โ โ0
โ (๐ + 0) = ๐) |
33 | 32 | fveq2d 6895 |
. . 3
โข (๐ โ โ0
โ (!โ(๐ + 0)) =
(!โ๐)) |
34 | 23, 31, 33 | 3brtr4d 5180 |
. 2
โข (๐ โ โ0
โ ((!โ๐)
ยท ((๐ + 1)โ0))
โค (!โ(๐ +
0))) |
35 | 22 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
36 | | peano2nn0 12511 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
37 | 36 | nn0red 12532 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
38 | | reexpcl 14043 |
. . . . . . . . 9
โข (((๐ + 1) โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
39 | 37, 38 | sylan 580 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + 1)โ๐) โ โ) |
40 | 35, 39 | remulcld 11243 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท ((๐ + 1)โ๐)) โ โ) |
41 | | nnnn0 12478 |
. . . . . . . . . . 11
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ0) |
42 | 41 | nn0ge0d 12534 |
. . . . . . . . . 10
โข
((!โ๐) โ
โ โ 0 โค (!โ๐)) |
43 | 21, 42 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ0
โ 0 โค (!โ๐)) |
44 | 43 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค (!โ๐)) |
45 | 37 | adantr 481 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + 1) โ โ) |
46 | | simpr 485 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ0) |
47 | 36 | nn0ge0d 12534 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 0 โค (๐ +
1)) |
48 | 47 | adantr 481 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค (๐ + 1)) |
49 | 45, 46, 48 | expge0d 14128 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค ((๐ + 1)โ๐)) |
50 | 35, 39, 44, 49 | mulge0d 11790 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค ((!โ๐) ยท ((๐ + 1)โ๐))) |
51 | 40, 50 | jca 512 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ๐) ยท ((๐ + 1)โ๐)) โ โ โง 0 โค
((!โ๐) ยท
((๐ + 1)โ๐)))) |
52 | | nn0addcl 12506 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
53 | 52 | faccld 14243 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(๐ + ๐)) โ โ) |
54 | 53 | nnred 12226 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(๐ + ๐)) โ โ) |
55 | | nn0re 12480 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
56 | | peano2nn0 12511 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
57 | 56 | nn0red 12532 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
58 | | readdcl 11192 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ + 1) โ โ) โ
(๐ + (๐ + 1)) โ โ) |
59 | 55, 57, 58 | syl2an 596 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + (๐ + 1)) โ โ) |
60 | 45, 48, 59 | jca31 515 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + 1) โ โ โง 0 โค (๐ + 1)) โง (๐ + (๐ + 1)) โ โ)) |
61 | 51, 54, 60 | jca31 515 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((((!โ๐) ยท ((๐ + 1)โ๐)) โ โ โง 0 โค
((!โ๐) ยท
((๐ + 1)โ๐))) โง (!โ(๐ + ๐)) โ โ) โง (((๐ + 1) โ โ โง 0 โค (๐ + 1)) โง (๐ + (๐ + 1)) โ โ))) |
62 | 61 | adantr 481 |
. . . 4
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ (((((!โ๐) ยท ((๐ + 1)โ๐)) โ โ โง 0 โค
((!โ๐) ยท
((๐ + 1)โ๐))) โง (!โ(๐ + ๐)) โ โ) โง (((๐ + 1) โ โ โง 0 โค (๐ + 1)) โง (๐ + (๐ + 1)) โ โ))) |
63 | 32 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + 0) = ๐) |
64 | | nn0ge0 12496 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 0 โค ๐) |
65 | 64 | adantl 482 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค ๐) |
66 | | 0re 11215 |
. . . . . . . . . 10
โข 0 โ
โ |
67 | | nn0re 12480 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
68 | 67 | adantl 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
69 | 55 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
70 | | leadd2 11682 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐
โ โ โง ๐
โ โ) โ (0 โค ๐ โ (๐ + 0) โค (๐ + ๐))) |
71 | 66, 68, 69, 70 | mp3an2i 1466 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0 โค ๐ โ (๐ + 0) โค (๐ + ๐))) |
72 | 65, 71 | mpbid 231 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + 0) โค (๐ + ๐)) |
73 | 63, 72 | eqbrtrrd 5172 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โค (๐ + ๐)) |
74 | 52 | nn0red 12532 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ โ) |
75 | | 1re 11213 |
. . . . . . . . 9
โข 1 โ
โ |
76 | | leadd1 11681 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ + ๐) โ โ โง 1 โ โ)
โ (๐ โค (๐ + ๐) โ (๐ + 1) โค ((๐ + ๐) + 1))) |
77 | 75, 76 | mp3an3 1450 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ + ๐) โ โ) โ (๐ โค (๐ + ๐) โ (๐ + 1) โค ((๐ + ๐) + 1))) |
78 | 69, 74, 77 | syl2anc 584 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค (๐ + ๐) โ (๐ + 1) โค ((๐ + ๐) + 1))) |
79 | 73, 78 | mpbid 231 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + 1) โค ((๐ + ๐) + 1)) |
80 | | nn0cn 12481 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ) |
81 | | ax-1cn 11167 |
. . . . . . . 8
โข 1 โ
โ |
82 | | addass 11196 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
83 | 81, 82 | mp3an3 1450 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
84 | 24, 80, 83 | syl2an 596 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
85 | 79, 84 | breqtrd 5174 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + 1) โค (๐ + (๐ + 1))) |
86 | 85 | anim1ci 616 |
. . . 4
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ (((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐)) โง (๐ + 1) โค (๐ + (๐ + 1)))) |
87 | | lemul12a 12071 |
. . . 4
โข
((((((!โ๐)
ยท ((๐ +
1)โ๐)) โ โ
โง 0 โค ((!โ๐)
ยท ((๐ +
1)โ๐))) โง
(!โ(๐ + ๐)) โ โ) โง
(((๐ + 1) โ โ
โง 0 โค (๐ + 1)) โง
(๐ + (๐ + 1)) โ โ)) โ
((((!โ๐) ยท
((๐ + 1)โ๐)) โค (!โ(๐ + ๐)) โง (๐ + 1) โค (๐ + (๐ + 1))) โ (((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1)) โค ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1))))) |
88 | 62, 86, 87 | sylc 65 |
. . 3
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ (((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1)) โค ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1)))) |
89 | | expp1 14033 |
. . . . . . 7
โข (((๐ + 1) โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ(๐ + 1)) = (((๐ + 1)โ๐) ยท (๐ + 1))) |
90 | 26, 89 | sylan 580 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + 1)โ(๐ + 1)) = (((๐ + 1)โ๐) ยท (๐ + 1))) |
91 | 90 | oveq2d 7424 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) = ((!โ๐) ยท (((๐ + 1)โ๐) ยท (๐ + 1)))) |
92 | 29 | adantr 481 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
93 | | expcl 14044 |
. . . . . . 7
โข (((๐ + 1) โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
94 | 26, 93 | sylan 580 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + 1)โ๐) โ โ) |
95 | 26 | adantr 481 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + 1) โ โ) |
96 | 92, 94, 95 | mulassd 11236 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1)) = ((!โ๐) ยท (((๐ + 1)โ๐) ยท (๐ + 1)))) |
97 | 91, 96 | eqtr4d 2775 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) = (((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1))) |
98 | 97 | adantr 481 |
. . 3
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ ((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) = (((!โ๐) ยท ((๐ + 1)โ๐)) ยท (๐ + 1))) |
99 | | facp1 14237 |
. . . . . 6
โข ((๐ + ๐) โ โ0 โ
(!โ((๐ + ๐) + 1)) = ((!โ(๐ + ๐)) ยท ((๐ + ๐) + 1))) |
100 | 52, 99 | syl 17 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ((๐ + ๐) + 1)) = ((!โ(๐ + ๐)) ยท ((๐ + ๐) + 1))) |
101 | 84 | fveq2d 6895 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ((๐ + ๐) + 1)) = (!โ(๐ + (๐ + 1)))) |
102 | 84 | oveq2d 7424 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ(๐ + ๐)) ยท ((๐ + ๐) + 1)) = ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1)))) |
103 | 100, 101,
102 | 3eqtr3d 2780 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(๐ + (๐ + 1))) = ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1)))) |
104 | 103 | adantr 481 |
. . 3
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ (!โ(๐ + (๐ + 1))) = ((!โ(๐ + ๐)) ยท (๐ + (๐ + 1)))) |
105 | 88, 98, 104 | 3brtr4d 5180 |
. 2
โข (((๐ โ โ0
โง ๐ โ
โ0) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ ((!โ๐) ยท ((๐ + 1)โ(๐ + 1))) โค (!โ(๐ + (๐ + 1)))) |
106 | 5, 10, 15, 20, 34, 105 | nn0indd 12658 |
1
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) |