Metamath Proof Explorer


Theorem slotsbhcdifOLD

Description: Obsolete proof of slotsbhcdif as of 28-Oct-2024. The slots Base , Hom and comp are different. (Contributed by AV, 5-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion slotsbhcdifOLD BasendxHomndxBasendxcompndxHomndxcompndx

Proof

Step Hyp Ref Expression
1 df-base Base=Slot1
2 1nn 1
3 1 2 ndxarg Basendx=1
4 1re 1
5 4nn0 40
6 1nn0 10
7 1lt10 1<10
8 2 5 6 7 declti 1<14
9 4 8 ltneii 114
10 homndx Homndx=14
11 9 10 neeqtrri 1Homndx
12 3 11 eqnetri BasendxHomndx
13 5nn0 50
14 2 13 6 7 declti 1<15
15 4 14 ltneii 115
16 ccondx compndx=15
17 15 16 neeqtrri 1compndx
18 3 17 eqnetri Basendxcompndx
19 6 5 deccl 140
20 19 nn0rei 14
21 5nn 5
22 4lt5 4<5
23 6 5 21 22 declt 14<15
24 20 23 ltneii 1415
25 24 16 neeqtrri 14compndx
26 10 25 eqnetri Homndxcompndx
27 12 18 26 3pm3.2i BasendxHomndxBasendxcompndxHomndxcompndx