Step | Hyp | Ref
| Expression |
1 | | prarloclemarch 7419 |
. . 3
โข ((๐ด โ Q โง
๐ถ โ Q)
โ โ๐ง โ
N ๐ด
<Q ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ)) |
2 | 1 | 3adant2 1016 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ โ๐ง โ N ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ)) |
3 | | pinn 7310 |
. . . . . . . 8
โข (๐ง โ N โ
๐ง โ
ฯ) |
4 | | 1pi 7316 |
. . . . . . . . . . . 12
โข
1o โ N |
5 | 4 | elexi 2751 |
. . . . . . . . . . 11
โข
1o โ V |
6 | 5 | sucid 4419 |
. . . . . . . . . 10
โข
1o โ suc 1o |
7 | | df-2o 6420 |
. . . . . . . . . 10
โข
2o = suc 1o |
8 | 6, 7 | eleqtrri 2253 |
. . . . . . . . 9
โข
1o โ 2o |
9 | | 2onn 6524 |
. . . . . . . . . . 11
โข
2o โ ฯ |
10 | | nnaword2 6517 |
. . . . . . . . . . 11
โข
((2o โ ฯ โง ๐ง โ ฯ) โ 2o โ
(๐ง +o
2o)) |
11 | 9, 10 | mpan 424 |
. . . . . . . . . 10
โข (๐ง โ ฯ โ
2o โ (๐ง
+o 2o)) |
12 | 11 | sseld 3156 |
. . . . . . . . 9
โข (๐ง โ ฯ โ
(1o โ 2o โ 1o โ (๐ง +o
2o))) |
13 | 8, 12 | mpi 15 |
. . . . . . . 8
โข (๐ง โ ฯ โ
1o โ (๐ง
+o 2o)) |
14 | 3, 13 | syl 14 |
. . . . . . 7
โข (๐ง โ N โ
1o โ (๐ง
+o 2o)) |
15 | | o1p1e2 6471 |
. . . . . . . . 9
โข
(1o +o 1o) =
2o |
16 | | addpiord 7317 |
. . . . . . . . . . 11
โข
((1o โ N โง 1o โ
N) โ (1o +N
1o) = (1o +o 1o)) |
17 | 4, 4, 16 | mp2an 426 |
. . . . . . . . . 10
โข
(1o +N 1o) =
(1o +o 1o) |
18 | | addclpi 7328 |
. . . . . . . . . . 11
โข
((1o โ N โง 1o โ
N) โ (1o +N
1o) โ N) |
19 | 4, 4, 18 | mp2an 426 |
. . . . . . . . . 10
โข
(1o +N 1o) โ
N |
20 | 17, 19 | eqeltrri 2251 |
. . . . . . . . 9
โข
(1o +o 1o) โ
N |
21 | 15, 20 | eqeltrri 2251 |
. . . . . . . 8
โข
2o โ N |
22 | | addpiord 7317 |
. . . . . . . 8
โข ((๐ง โ N โง
2o โ N) โ (๐ง +N 2o) =
(๐ง +o
2o)) |
23 | 21, 22 | mpan2 425 |
. . . . . . 7
โข (๐ง โ N โ
(๐ง
+N 2o) = (๐ง +o
2o)) |
24 | 14, 23 | eleqtrrd 2257 |
. . . . . 6
โข (๐ง โ N โ
1o โ (๐ง
+N 2o)) |
25 | | addclpi 7328 |
. . . . . . . 8
โข ((๐ง โ N โง
2o โ N) โ (๐ง +N 2o)
โ N) |
26 | 21, 25 | mpan2 425 |
. . . . . . 7
โข (๐ง โ N โ
(๐ง
+N 2o) โ
N) |
27 | | ltpiord 7320 |
. . . . . . . 8
โข
((1o โ N โง (๐ง +N 2o)
โ N) โ (1o <N
(๐ง
+N 2o) โ 1o โ (๐ง +N
2o))) |
28 | 4, 27 | mpan 424 |
. . . . . . 7
โข ((๐ง +N
2o) โ N โ (1o
<N (๐ง +N 2o)
โ 1o โ (๐ง +N
2o))) |
29 | 26, 28 | syl 14 |
. . . . . 6
โข (๐ง โ N โ
(1o <N (๐ง +N 2o)
โ 1o โ (๐ง +N
2o))) |
30 | 24, 29 | mpbird 167 |
. . . . 5
โข (๐ง โ N โ
1o <N (๐ง +N
2o)) |
31 | 30 | adantl 277 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ 1o <N
(๐ง
+N 2o)) |
32 | 31 | adantrr 479 |
. . 3
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ 1o
<N (๐ง +N
2o)) |
33 | | nna0 6477 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ ฯ โ (๐ง +o โ
) = ๐ง) |
34 | | 0lt1o 6443 |
. . . . . . . . . . . . . . . . . . . 20
โข โ
โ 1o |
35 | | 1on 6426 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
1o โ On |
36 | 35 | onsuci 4517 |
. . . . . . . . . . . . . . . . . . . . 21
โข suc
1o โ On |
37 | | ontr1 4391 |
. . . . . . . . . . . . . . . . . . . . 21
โข (suc
1o โ On โ ((โ
โ 1o โง
1o โ suc 1o) โ โ
โ suc
1o)) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
โข ((โ
โ 1o โง 1o โ suc 1o) โ
โ
โ suc 1o) |
39 | 34, 6, 38 | mp2an 426 |
. . . . . . . . . . . . . . . . . . 19
โข โ
โ suc 1o |
40 | 39, 7 | eleqtrri 2253 |
. . . . . . . . . . . . . . . . . 18
โข โ
โ 2o |
41 | | nnaordi 6511 |
. . . . . . . . . . . . . . . . . . 19
โข
((2o โ ฯ โง ๐ง โ ฯ) โ (โ
โ
2o โ (๐ง
+o โ
) โ (๐ง +o
2o))) |
42 | 9, 41 | mpan 424 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง โ ฯ โ (โ
โ 2o โ (๐ง +o โ
) โ (๐ง +o
2o))) |
43 | 40, 42 | mpi 15 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ ฯ โ (๐ง +o โ
) โ
(๐ง +o
2o)) |
44 | 33, 43 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ ฯ โ ๐ง โ (๐ง +o
2o)) |
45 | 3, 44 | syl 14 |
. . . . . . . . . . . . . . 15
โข (๐ง โ N โ
๐ง โ (๐ง +o
2o)) |
46 | 45, 23 | eleqtrrd 2257 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
๐ง โ (๐ง +N
2o)) |
47 | | ltpiord 7320 |
. . . . . . . . . . . . . . 15
โข ((๐ง โ N โง
(๐ง
+N 2o) โ N) โ
(๐ง
<N (๐ง +N 2o)
โ ๐ง โ (๐ง +N
2o))) |
48 | 26, 47 | mpdan 421 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
(๐ง
<N (๐ง +N 2o)
โ ๐ง โ (๐ง +N
2o))) |
49 | 46, 48 | mpbird 167 |
. . . . . . . . . . . . 13
โข (๐ง โ N โ
๐ง
<N (๐ง +N
2o)) |
50 | | mulidpi 7319 |
. . . . . . . . . . . . 13
โข (๐ง โ N โ
(๐ง
ยทN 1o) = ๐ง) |
51 | | mulcompig 7332 |
. . . . . . . . . . . . . . . 16
โข (((๐ง +N
2o) โ N โง 1o โ
N) โ ((๐ง
+N 2o) ยทN
1o) = (1o ยทN (๐ง +N
2o))) |
52 | 4, 51 | mpan2 425 |
. . . . . . . . . . . . . . 15
โข ((๐ง +N
2o) โ N โ ((๐ง +N 2o)
ยทN 1o) = (1o
ยทN (๐ง +N
2o))) |
53 | 26, 52 | syl 14 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
((๐ง
+N 2o) ยทN
1o) = (1o ยทN (๐ง +N
2o))) |
54 | | mulidpi 7319 |
. . . . . . . . . . . . . . 15
โข ((๐ง +N
2o) โ N โ ((๐ง +N 2o)
ยทN 1o) = (๐ง +N
2o)) |
55 | 26, 54 | syl 14 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
((๐ง
+N 2o) ยทN
1o) = (๐ง
+N 2o)) |
56 | 53, 55 | eqtr3d 2212 |
. . . . . . . . . . . . 13
โข (๐ง โ N โ
(1o ยทN (๐ง +N 2o))
= (๐ง
+N 2o)) |
57 | 49, 50, 56 | 3brtr4d 4037 |
. . . . . . . . . . . 12
โข (๐ง โ N โ
(๐ง
ยทN 1o)
<N (1o
ยทN (๐ง +N
2o))) |
58 | | ordpipqqs 7375 |
. . . . . . . . . . . . . . 15
โข (((๐ง โ N โง
1o โ N) โง ((๐ง +N 2o)
โ N โง 1o โ N)) โ
([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ง ยทN
1o) <N (1o
ยทN (๐ง +N
2o)))) |
59 | 4, 58 | mpanl2 435 |
. . . . . . . . . . . . . 14
โข ((๐ง โ N โง
((๐ง
+N 2o) โ N โง
1o โ N)) โ ([โจ๐ง, 1oโฉ]
~Q <Q [โจ(๐ง +N
2o), 1oโฉ] ~Q โ (๐ง
ยทN 1o)
<N (1o
ยทN (๐ง +N
2o)))) |
60 | 4, 59 | mpanr2 438 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
(๐ง
+N 2o) โ N) โ
([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ง ยทN
1o) <N (1o
ยทN (๐ง +N
2o)))) |
61 | 26, 60 | mpdan 421 |
. . . . . . . . . . . 12
โข (๐ง โ N โ
([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ง ยทN
1o) <N (1o
ยทN (๐ง +N
2o)))) |
62 | 57, 61 | mpbird 167 |
. . . . . . . . . . 11
โข (๐ง โ N โ
[โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ) |
63 | 62 | adantl 277 |
. . . . . . . . . 10
โข ((๐ถ โ Q โง
๐ง โ N)
โ [โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ) |
64 | | opelxpi 4660 |
. . . . . . . . . . . . . . . 16
โข (((๐ง +N
2o) โ N โง 1o โ
N) โ โจ(๐ง +N 2o),
1oโฉ โ (N ร
N)) |
65 | 4, 64 | mpan2 425 |
. . . . . . . . . . . . . . 15
โข ((๐ง +N
2o) โ N โ โจ(๐ง +N 2o),
1oโฉ โ (N ร
N)) |
66 | | enqex 7361 |
. . . . . . . . . . . . . . . 16
โข
~Q โ V |
67 | 66 | ecelqsi 6591 |
. . . . . . . . . . . . . . 15
โข
(โจ(๐ง
+N 2o), 1oโฉ โ
(N ร N) โ [โจ(๐ง +N 2o),
1oโฉ] ~Q โ ((N
ร N) / ~Q
)) |
68 | 26, 65, 67 | 3syl 17 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ ((N ร N)
/ ~Q )) |
69 | | df-nqqs 7349 |
. . . . . . . . . . . . . 14
โข
Q = ((N ร N) /
~Q ) |
70 | 68, 69 | eleqtrrdi 2271 |
. . . . . . . . . . . . 13
โข (๐ง โ N โ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ Q) |
71 | | opelxpi 4660 |
. . . . . . . . . . . . . . . . 17
โข ((๐ง โ N โง
1o โ N) โ โจ๐ง, 1oโฉ โ (N
ร N)) |
72 | 4, 71 | mpan2 425 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ N โ
โจ๐ง,
1oโฉ โ (N ร
N)) |
73 | 66 | ecelqsi 6591 |
. . . . . . . . . . . . . . . 16
โข
(โจ๐ง,
1oโฉ โ (N ร N) โ
[โจ๐ง,
1oโฉ] ~Q โ ((N
ร N) / ~Q
)) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . 15
โข (๐ง โ N โ
[โจ๐ง,
1oโฉ] ~Q โ ((N
ร N) / ~Q
)) |
75 | 74, 69 | eleqtrrdi 2271 |
. . . . . . . . . . . . . 14
โข (๐ง โ N โ
[โจ๐ง,
1oโฉ] ~Q โ
Q) |
76 | | ltmnqg 7402 |
. . . . . . . . . . . . . 14
โข
(([โจ๐ง,
1oโฉ] ~Q โ Q โง
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ Q โง ๐ถ โ Q) โ
([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ถ ยทQ
[โจ๐ง,
1oโฉ] ~Q )
<Q (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ))) |
77 | 75, 76 | syl3an1 1271 |
. . . . . . . . . . . . 13
โข ((๐ง โ N โง
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ Q โง ๐ถ โ Q) โ
([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ถ ยทQ
[โจ๐ง,
1oโฉ] ~Q )
<Q (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ))) |
78 | 70, 77 | syl3an2 1272 |
. . . . . . . . . . . 12
โข ((๐ง โ N โง
๐ง โ N
โง ๐ถ โ
Q) โ ([โจ๐ง, 1oโฉ]
~Q <Q [โจ(๐ง +N
2o), 1oโฉ] ~Q โ (๐ถ
ยทQ [โจ๐ง, 1oโฉ]
~Q ) <Q (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ))) |
79 | 78 | 3anidm12 1295 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ถ โ Q)
โ ([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ถ ยทQ
[โจ๐ง,
1oโฉ] ~Q )
<Q (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ))) |
80 | 79 | ancoms 268 |
. . . . . . . . . 10
โข ((๐ถ โ Q โง
๐ง โ N)
โ ([โจ๐ง,
1oโฉ] ~Q <Q
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ (๐ถ ยทQ
[โจ๐ง,
1oโฉ] ~Q )
<Q (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ))) |
81 | 63, 80 | mpbid 147 |
. . . . . . . . 9
โข ((๐ถ โ Q โง
๐ง โ N)
โ (๐ถ
ยทQ [โจ๐ง, 1oโฉ]
~Q ) <Q (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q )) |
82 | | mulcomnqg 7384 |
. . . . . . . . . 10
โข ((๐ถ โ Q โง
[โจ๐ง,
1oโฉ] ~Q โ Q) โ
(๐ถ
ยทQ [โจ๐ง, 1oโฉ]
~Q ) = ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ)) |
83 | 75, 82 | sylan2 286 |
. . . . . . . . 9
โข ((๐ถ โ Q โง
๐ง โ N)
โ (๐ถ
ยทQ [โจ๐ง, 1oโฉ]
~Q ) = ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ)) |
84 | | mulcomnqg 7384 |
. . . . . . . . . 10
โข ((๐ถ โ Q โง
[โจ(๐ง
+N 2o), 1oโฉ]
~Q โ Q) โ (๐ถ ยทQ
[โจ(๐ง
+N 2o), 1oโฉ]
~Q ) = ([โจ(๐ง +N 2o),
1oโฉ] ~Q
ยทQ ๐ถ)) |
85 | 70, 84 | sylan2 286 |
. . . . . . . . 9
โข ((๐ถ โ Q โง
๐ง โ N)
โ (๐ถ
ยทQ [โจ(๐ง +N 2o),
1oโฉ] ~Q ) = ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ)) |
86 | 81, 83, 85 | 3brtr3d 4036 |
. . . . . . . 8
โข ((๐ถ โ Q โง
๐ง โ N)
โ ([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)) |
87 | 86 | 3ad2antl3 1161 |
. . . . . . 7
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)) |
88 | 87 | adantrr 479 |
. . . . . 6
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)) |
89 | | ltsonq 7399 |
. . . . . . . . . 10
โข
<Q Or Q |
90 | | ltrelnq 7366 |
. . . . . . . . . 10
โข
<Q โ (Q ร
Q) |
91 | 89, 90 | sotri 5026 |
. . . . . . . . 9
โข ((๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ) โง ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)) โ ๐ด <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)) |
92 | 91 | ex 115 |
. . . . . . . 8
โข (๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ) โ (([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ ๐ด <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ))) |
93 | 92 | adantl 277 |
. . . . . . 7
โข ((๐ง โ N โง
๐ด
<Q ([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ)) โ (([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ ๐ด <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ))) |
94 | 93 | adantl 277 |
. . . . . 6
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ (([โจ๐ง, 1oโฉ]
~Q ยทQ ๐ถ) <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ ๐ด <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ))) |
95 | 88, 94 | mpd 13 |
. . . . 5
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ ๐ด <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)) |
96 | | mulclnq 7377 |
. . . . . . . . . 10
โข
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q โ Q โง ๐ถ โ Q) โ
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ
Q) |
97 | 70, 96 | sylan 283 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ถ โ Q)
โ ([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ
Q) |
98 | 97 | ancoms 268 |
. . . . . . . 8
โข ((๐ถ โ Q โง
๐ง โ N)
โ ([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ
Q) |
99 | 98 | 3ad2antl3 1161 |
. . . . . . 7
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ ([โจ(๐ง +N 2o),
1oโฉ] ~Q
ยทQ ๐ถ) โ Q) |
100 | | simpl2 1001 |
. . . . . . 7
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ ๐ต โ Q) |
101 | | ltaddnq 7408 |
. . . . . . 7
โข
((([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ Q โง
๐ต โ Q)
โ ([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต)) |
102 | 99, 100, 101 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ ([โจ(๐ง +N 2o),
1oโฉ] ~Q
ยทQ ๐ถ) <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต)) |
103 | 102 | adantrr 479 |
. . . . 5
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ ([โจ(๐ง +N 2o),
1oโฉ] ~Q
ยทQ ๐ถ) <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต)) |
104 | 89, 90 | sotri 5026 |
. . . . 5
โข ((๐ด <Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โง ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ) <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต)) โ ๐ด <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต)) |
105 | 95, 103, 104 | syl2anc 411 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ ๐ด <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต)) |
106 | | addcomnqg 7382 |
. . . . . . 7
โข
((([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) โ Q โง
๐ต โ Q)
โ (([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต) = (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ))) |
107 | 99, 100, 106 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ (([โจ(๐ง +N 2o),
1oโฉ] ~Q
ยทQ ๐ถ) +Q ๐ต) = (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ))) |
108 | 107 | breq2d 4017 |
. . . . 5
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ (๐ด <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต) โ ๐ด <Q (๐ต +Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)))) |
109 | 108 | adantrr 479 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ (๐ด <Q
(([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ) +Q
๐ต) โ ๐ด <Q (๐ต +Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)))) |
110 | 105, 109 | mpbid 147 |
. . 3
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ ๐ด <Q (๐ต +Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ))) |
111 | | simpr 110 |
. . . . 5
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ ๐ง โ N) |
112 | | breq2 4009 |
. . . . . . . 8
โข (๐ฅ = (๐ง +N 2o)
โ (1o <N ๐ฅ โ 1o
<N (๐ง +N
2o))) |
113 | | opeq1 3780 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ง +N 2o)
โ โจ๐ฅ,
1oโฉ = โจ(๐ง +N 2o),
1oโฉ) |
114 | 113 | eceq1d 6573 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ง +N 2o)
โ [โจ๐ฅ,
1oโฉ] ~Q = [โจ(๐ง +N 2o),
1oโฉ] ~Q ) |
115 | 114 | oveq1d 5892 |
. . . . . . . . . 10
โข (๐ฅ = (๐ง +N 2o)
โ ([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ) = ([โจ(๐ง +N 2o),
1oโฉ] ~Q
ยทQ ๐ถ)) |
116 | 115 | oveq2d 5893 |
. . . . . . . . 9
โข (๐ฅ = (๐ง +N 2o)
โ (๐ต
+Q ([โจ๐ฅ, 1oโฉ]
~Q ยทQ ๐ถ)) = (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ))) |
117 | 116 | breq2d 4017 |
. . . . . . . 8
โข (๐ฅ = (๐ง +N 2o)
โ (๐ด
<Q (๐ต +Q ([โจ๐ฅ, 1oโฉ]
~Q ยทQ ๐ถ)) โ ๐ด <Q (๐ต +Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ)))) |
118 | 112, 117 | anbi12d 473 |
. . . . . . 7
โข (๐ฅ = (๐ง +N 2o)
โ ((1o <N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ))) โ (1o
<N (๐ง +N 2o)
โง ๐ด
<Q (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ))))) |
119 | 118 | rspcev 2843 |
. . . . . 6
โข (((๐ง +N
2o) โ N โง (1o
<N (๐ง +N 2o)
โง ๐ด
<Q (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ)))) โ โ๐ฅ โ N (1o
<N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ)))) |
120 | 119 | ex 115 |
. . . . 5
โข ((๐ง +N
2o) โ N โ ((1o
<N (๐ง +N 2o)
โง ๐ด
<Q (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ))) โ โ๐ฅ โ N (1o
<N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ))))) |
121 | 111, 26, 120 | 3syl 17 |
. . . 4
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง ๐ง
โ N) โ ((1o <N
(๐ง
+N 2o) โง ๐ด <Q (๐ต +Q
([โจ(๐ง
+N 2o), 1oโฉ]
~Q ยทQ ๐ถ))) โ โ๐ฅ โ N
(1o <N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ))))) |
122 | 121 | adantrr 479 |
. . 3
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ ((1o
<N (๐ง +N 2o)
โง ๐ด
<Q (๐ต +Q ([โจ(๐ง +N
2o), 1oโฉ] ~Q
ยทQ ๐ถ))) โ โ๐ฅ โ N (1o
<N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ))))) |
123 | 32, 110, 122 | mp2and 433 |
. 2
โข (((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โง (๐ง
โ N โง ๐ด <Q
([โจ๐ง,
1oโฉ] ~Q
ยทQ ๐ถ))) โ โ๐ฅ โ N (1o
<N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ)))) |
124 | 2, 123 | rexlimddv 2599 |
1
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ โ๐ฅ โ N (1o
<N ๐ฅ โง ๐ด <Q (๐ต +Q
([โจ๐ฅ,
1oโฉ] ~Q
ยทQ ๐ถ)))) |