Proof of Theorem axlowdimlem13
Step | Hyp | Ref
| Expression |
1 | | 2ne0 11113 |
. . . . . . . . 9
|
2 | 1 | neii 2796 |
. . . . . . . 8
|
3 | | eqcom 2629 |
. . . . . . . . 9
|
4 | | 1pneg1e0 11129 |
. . . . . . . . . . 11
|
5 | 4 | eqcomi 2631 |
. . . . . . . . . 10
|
6 | | df-2 11079 |
. . . . . . . . . 10
|
7 | 5, 6 | eqeq12i 2636 |
. . . . . . . . 9
|
8 | | ax-1cn 9994 |
. . . . . . . . . 10
|
9 | | neg1cn 11124 |
. . . . . . . . . 10
|
10 | 8, 9, 8 | addcani 10229 |
. . . . . . . . 9
|
11 | 3, 7, 10 | 3bitri 286 |
. . . . . . . 8
|
12 | 2, 11 | mtbi 312 |
. . . . . . 7
|
13 | 12 | intnanr 961 |
. . . . . 6
|
14 | | ax-1ne0 10005 |
. . . . . . . . 9
|
15 | 14 | neii 2796 |
. . . . . . . 8
|
16 | | negeq0 10335 |
. . . . . . . . 9
|
17 | 8, 16 | ax-mp 5 |
. . . . . . . 8
|
18 | 15, 17 | mtbi 312 |
. . . . . . 7
|
19 | 18 | intnanr 961 |
. . . . . 6
|
20 | 13, 19 | pm3.2ni 899 |
. . . . 5
|
21 | | negex 10279 |
. . . . . 6
|
22 | | c0ex 10034 |
. . . . . 6
|
23 | | 1ex 10035 |
. . . . . 6
|
24 | 21, 22, 23, 22 | preq12b 4382 |
. . . . 5
|
25 | 20, 24 | mtbir 313 |
. . . 4
|
26 | | 3ex 11096 |
. . . . . . . . 9
|
27 | 26 | rnsnop 5616 |
. . . . . . . 8
|
28 | 27 | a1i 11 |
. . . . . . 7
|
29 | | elnnuz 11724 |
. . . . . . . . . . . 12
|
30 | | eluzfz1 12348 |
. . . . . . . . . . . 12
|
31 | 29, 30 | sylbi 207 |
. . . . . . . . . . 11
|
32 | | df-3 11080 |
. . . . . . . . . . . . . . . 16
|
33 | | 1e0p1 11552 |
. . . . . . . . . . . . . . . 16
|
34 | 32, 33 | eqeq12i 2636 |
. . . . . . . . . . . . . . 15
|
35 | | 2cn 11091 |
. . . . . . . . . . . . . . . 16
|
36 | | 0cn 10032 |
. . . . . . . . . . . . . . . 16
|
37 | 35, 36, 8 | addcan2i 10230 |
. . . . . . . . . . . . . . 15
|
38 | 34, 37 | bitri 264 |
. . . . . . . . . . . . . 14
|
39 | 38 | necon3bii 2846 |
. . . . . . . . . . . . 13
|
40 | 1, 39 | mpbir 221 |
. . . . . . . . . . . 12
|
41 | 40 | necomi 2848 |
. . . . . . . . . . 11
|
42 | 31, 41 | jctir 561 |
. . . . . . . . . 10
|
43 | | eldifsn 4317 |
. . . . . . . . . 10
|
44 | 42, 43 | sylibr 224 |
. . . . . . . . 9
|
45 | 44 | adantr 481 |
. . . . . . . 8
|
46 | | ne0i 3921 |
. . . . . . . 8
|
47 | | rnxp 5564 |
. . . . . . . 8
|
48 | 45, 46, 47 | 3syl 18 |
. . . . . . 7
|
49 | 28, 48 | uneq12d 3768 |
. . . . . 6
|
50 | | rnun 5541 |
. . . . . 6
|
51 | | df-pr 4180 |
. . . . . 6
|
52 | 49, 50, 51 | 3eqtr4g 2681 |
. . . . 5
|
53 | | ovex 6678 |
. . . . . . . . 9
|
54 | 53 | rnsnop 5616 |
. . . . . . . 8
|
55 | 54 | a1i 11 |
. . . . . . 7
|
56 | | nnz 11399 |
. . . . . . . . . . 11
|
57 | | fzssp1 12384 |
. . . . . . . . . . . 12
|
58 | | zcn 11382 |
. . . . . . . . . . . . 13
|
59 | | npcan1 10455 |
. . . . . . . . . . . . . 14
|
60 | 59 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
61 | 58, 60 | syl 17 |
. . . . . . . . . . . 12
|
62 | 57, 61 | syl5sseq 3653 |
. . . . . . . . . . 11
|
63 | 56, 62 | syl 17 |
. . . . . . . . . 10
|
64 | 63 | sselda 3603 |
. . . . . . . . 9
|
65 | | elfzelz 12342 |
. . . . . . . . . . . 12
|
66 | 65 | zred 11482 |
. . . . . . . . . . 11
|
67 | | id 22 |
. . . . . . . . . . . 12
|
68 | | ltp1 10861 |
. . . . . . . . . . . 12
|
69 | 67, 68 | ltned 10173 |
. . . . . . . . . . 11
|
70 | 66, 69 | syl 17 |
. . . . . . . . . 10
|
71 | 70 | adantl 482 |
. . . . . . . . 9
|
72 | | eldifsn 4317 |
. . . . . . . . 9
|
73 | 64, 71, 72 | sylanbrc 698 |
. . . . . . . 8
|
74 | | ne0i 3921 |
. . . . . . . 8
|
75 | | rnxp 5564 |
. . . . . . . 8
|
76 | 73, 74, 75 | 3syl 18 |
. . . . . . 7
|
77 | 55, 76 | uneq12d 3768 |
. . . . . 6
|
78 | | rnun 5541 |
. . . . . 6
|
79 | | df-pr 4180 |
. . . . . 6
|
80 | 77, 78, 79 | 3eqtr4g 2681 |
. . . . 5
|
81 | 52, 80 | eqeq12d 2637 |
. . . 4
|
82 | 25, 81 | mtbiri 317 |
. . 3
|
83 | | rneq 5351 |
. . 3
|
84 | 82, 83 | nsyl 135 |
. 2
|
85 | | axlowdimlem13.1 |
. . . 4
|
86 | | axlowdimlem13.2 |
. . . 4
|
87 | 85, 86 | eqeq12i 2636 |
. . 3
|
88 | 87 | necon3abii 2840 |
. 2
|
89 | 84, 88 | sylibr 224 |
1
|