Metamath Proof Explorer


Theorem metakunt7

Description: C is the left inverse for A. (Contributed by metakunt, 24-May-2024)

Ref Expression
Hypotheses metakunt7.1 φ M
metakunt7.2 φ I
metakunt7.3 φ I M
metakunt7.4 A = x 1 M if x = I M if x < I x x 1
metakunt7.5 C = y 1 M if y = M I if y < I y y + 1
metakunt7.6 φ X 1 M
Assertion metakunt7 φ I < X A X = X 1 ¬ A X = M ¬ A X < I

Proof

Step Hyp Ref Expression
1 metakunt7.1 φ M
2 metakunt7.2 φ I
3 metakunt7.3 φ I M
4 metakunt7.4 A = x 1 M if x = I M if x < I x x 1
5 metakunt7.5 C = y 1 M if y = M I if y < I y y + 1
6 metakunt7.6 φ X 1 M
7 4 a1i φ I < X A = x 1 M if x = I M if x < I x x 1
8 eqeq1 x = X x = I X = I
9 breq1 x = X x < I X < I
10 id x = X x = X
11 oveq1 x = X x 1 = X 1
12 9 10 11 ifbieq12d x = X if x < I x x 1 = if X < I X X 1
13 8 12 ifbieq2d x = X if x = I M if x < I x x 1 = if X = I M if X < I X X 1
14 13 adantl φ I < X x = X if x = I M if x < I x x 1 = if X = I M if X < I X X 1
15 2 nnred φ I
16 15 adantr φ I < X I
17 simpr φ I < X I < X
18 16 17 ltned φ I < X I X
19 18 necomd φ I < X X I
20 df-ne X I ¬ X = I
21 19 20 sylib φ I < X ¬ X = I
22 iffalse ¬ X = I if X = I M if X < I X X 1 = if X < I X X 1
23 21 22 syl φ I < X if X = I M if X < I X X 1 = if X < I X X 1
24 elfznn X 1 M X
25 6 24 syl φ X
26 25 nnred φ X
27 26 adantr φ I < X X
28 16 27 17 ltled φ I < X I X
29 16 27 lenltd φ I < X I X ¬ X < I
30 28 29 mpbid φ I < X ¬ X < I
31 iffalse ¬ X < I if X < I X X 1 = X 1
32 30 31 syl φ I < X if X < I X X 1 = X 1
33 23 32 eqtrd φ I < X if X = I M if X < I X X 1 = X 1
34 33 adantr φ I < X x = X if X = I M if X < I X X 1 = X 1
35 14 34 eqtrd φ I < X x = X if x = I M if x < I x x 1 = X 1
36 6 adantr φ I < X X 1 M
37 36 elfzelzd φ I < X X
38 1zzd φ I < X 1
39 37 38 zsubcld φ I < X X 1
40 7 35 36 39 fvmptd φ I < X A X = X 1
41 1red φ 1
42 26 41 resubcld φ X 1
43 elfzle2 X 1 M X M
44 6 43 syl φ X M
45 6 elfzelzd φ X
46 1 nnzd φ M
47 zlem1lt X M X M X 1 < M
48 45 46 47 syl2anc φ X M X 1 < M
49 44 48 mpbid φ X 1 < M
50 42 49 ltned φ X 1 M
51 50 adantr φ I < X X 1 M
52 40 51 eqnetrd φ I < X A X M
53 52 neneqd φ I < X ¬ A X = M
54 2 nnzd φ I
55 zltlem1 I X I < X I X 1
56 55 biimpd I X I < X I X 1
57 54 45 56 syl2anc φ I < X I X 1
58 57 imp φ I < X I X 1
59 58 40 breqtrrd φ I < X I A X
60 39 zred φ I < X X 1
61 40 60 eqeltrd φ I < X A X
62 16 61 lenltd φ I < X I A X ¬ A X < I
63 59 62 mpbid φ I < X ¬ A X < I
64 40 53 63 3jca φ I < X A X = X 1 ¬ A X = M ¬ A X < I