Step | Hyp | Ref
| Expression |
1 | | r19.26 3064 |
. . . 4
|
2 | | simpr 477 |
. . . . . . . . . 10
|
3 | | simpl1 1064 |
. . . . . . . . . 10
|
4 | 2, 3 | pccld 15555 |
. . . . . . . . 9
|
5 | 4 | nn0red 11352 |
. . . . . . . 8
|
6 | | simpl2 1065 |
. . . . . . . . . 10
|
7 | 2, 6 | pccld 15555 |
. . . . . . . . 9
|
8 | 7 | nn0red 11352 |
. . . . . . . 8
|
9 | | 1red 10055 |
. . . . . . . 8
|
10 | | le2add 10510 |
. . . . . . . 8
|
11 | 5, 8, 9, 9, 10 | syl22anc 1327 |
. . . . . . 7
|
12 | | ax-1ne0 10005 |
. . . . . . . . . . . 12
|
13 | | simpl3 1066 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
15 | 3 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
16 | 6 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
17 | | pcgcd 15582 |
. . . . . . . . . . . . . . . 16
|
18 | 2, 15, 16, 17 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
19 | | pc1 15560 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | adantl 482 |
. . . . . . . . . . . . . . 15
|
21 | 14, 18, 20 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
|
22 | | ifid 4125 |
. . . . . . . . . . . . . . . 16
|
23 | | ifeq12 4103 |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
25 | 24 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
26 | 21, 25 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
|
27 | 26 | necon3ad 2807 |
. . . . . . . . . . . 12
|
28 | 12, 27 | mpi 20 |
. . . . . . . . . . 11
|
29 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
30 | 5 | recnd 10068 |
. . . . . . . . . . . . 13
|
31 | | subeq0 10307 |
. . . . . . . . . . . . 13
|
32 | 29, 30, 31 | sylancr 695 |
. . . . . . . . . . . 12
|
33 | 8 | recnd 10068 |
. . . . . . . . . . . . 13
|
34 | | subeq0 10307 |
. . . . . . . . . . . . 13
|
35 | 29, 33, 34 | sylancr 695 |
. . . . . . . . . . . 12
|
36 | 32, 35 | anbi12d 747 |
. . . . . . . . . . 11
|
37 | 28, 36 | mtbird 315 |
. . . . . . . . . 10
|
38 | 37 | adantr 481 |
. . . . . . . . 9
|
39 | | eqcom 2629 |
. . . . . . . . . . 11
|
40 | | 1re 10039 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40, 40 | readdcli 10053 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | recni 10052 |
. . . . . . . . . . . . . . . 16
|
43 | 4, 7 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . 18
|
44 | 43 | nn0red 11352 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
46 | | subeq0 10307 |
. . . . . . . . . . . . . . . 16
|
47 | 42, 45, 46 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
48 | 47, 39 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
49 | 9 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
50 | 49, 49, 30, 33 | addsub4d 10439 |
. . . . . . . . . . . . . . 15
|
51 | 50 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
52 | 48, 51 | bitr3d 270 |
. . . . . . . . . . . . 13
|
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
|
54 | | subge0 10541 |
. . . . . . . . . . . . . . . 16
|
55 | 40, 5, 54 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
56 | | subge0 10541 |
. . . . . . . . . . . . . . . 16
|
57 | 40, 8, 56 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
58 | 55, 57 | anbi12d 747 |
. . . . . . . . . . . . . 14
|
59 | | resubcl 10345 |
. . . . . . . . . . . . . . . 16
|
60 | 40, 5, 59 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
61 | | resubcl 10345 |
. . . . . . . . . . . . . . . 16
|
62 | 40, 8, 61 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
63 | | add20 10540 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | an4s 869 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | ex 450 |
. . . . . . . . . . . . . . 15
|
66 | 60, 62, 65 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
67 | 58, 66 | sylbird 250 |
. . . . . . . . . . . . 13
|
68 | 67 | imp 445 |
. . . . . . . . . . . 12
|
69 | 53, 68 | bitrd 268 |
. . . . . . . . . . 11
|
70 | 39, 69 | syl5bb 272 |
. . . . . . . . . 10
|
71 | 70 | necon3abid 2830 |
. . . . . . . . 9
|
72 | 38, 71 | mpbird 247 |
. . . . . . . 8
|
73 | 72 | ex 450 |
. . . . . . 7
|
74 | 11, 73 | jcad 555 |
. . . . . 6
|
75 | | nnz 11399 |
. . . . . . . . . . 11
|
76 | | nnne0 11053 |
. . . . . . . . . . 11
|
77 | 75, 76 | jca 554 |
. . . . . . . . . 10
|
78 | 3, 77 | syl 17 |
. . . . . . . . 9
|
79 | | nnz 11399 |
. . . . . . . . . . 11
|
80 | | nnne0 11053 |
. . . . . . . . . . 11
|
81 | 79, 80 | jca 554 |
. . . . . . . . . 10
|
82 | 6, 81 | syl 17 |
. . . . . . . . 9
|
83 | | pcmul 15556 |
. . . . . . . . 9
|
84 | 2, 78, 82, 83 | syl3anc 1326 |
. . . . . . . 8
|
85 | 84 | breq1d 4663 |
. . . . . . 7
|
86 | | 1nn0 11308 |
. . . . . . . 8
|
87 | | nn0leltp1 11436 |
. . . . . . . 8
|
88 | 43, 86, 87 | sylancl 694 |
. . . . . . 7
|
89 | | ltlen 10138 |
. . . . . . . 8
|
90 | 44, 41, 89 | sylancl 694 |
. . . . . . 7
|
91 | 85, 88, 90 | 3bitrd 294 |
. . . . . 6
|
92 | 74, 91 | sylibrd 249 |
. . . . 5
|
93 | 92 | ralimdva 2962 |
. . . 4
|
94 | 1, 93 | syl5bir 233 |
. . 3
|
95 | | issqf 24862 |
. . . . 5
|
96 | | issqf 24862 |
. . . . 5
|
97 | 95, 96 | bi2anan9 917 |
. . . 4
|
98 | 97 | 3adant3 1081 |
. . 3
|
99 | | nnmulcl 11043 |
. . . . 5
|
100 | 99 | 3adant3 1081 |
. . . 4
|
101 | | issqf 24862 |
. . . 4
|
102 | 100, 101 | syl 17 |
. . 3
|
103 | 94, 98, 102 | 3imtr4d 283 |
. 2
|
104 | 103 | imp 445 |
1
|