Metamath Proof Explorer

Theorem jm2.24

Description: Lemma 2.24 of JonesMatijasevic p. 697 extended to ZZ . Could be eliminated with a more careful proof of jm2.26lem3 . (Contributed by Stefan O'Rear, 3-Oct-2014)

Ref Expression
Assertion jm2.24 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
3 2 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝑁 − 1 ) ∈ ℤ )
4 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
5 4 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
6 1 3 5 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
7 6 zred ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℝ )
8 4 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
9 8 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℝ )
10 9 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℝ )
11 7 10 readdcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ∈ ℝ )
12 0red ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 ∈ ℝ )
13 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
14 13 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
16 15 nn0red ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Xrm 𝑁 ) ∈ ℝ )
17 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
18 17 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → - 𝑁 ∈ ℤ )
19 18 peano2zd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( - 𝑁 + 1 ) ∈ ℤ )
20 4 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( - 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( - 𝑁 + 1 ) ) ∈ ℤ )
21 1 19 20 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm ( - 𝑁 + 1 ) ) ∈ ℤ )
22 21 zred ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm ( - 𝑁 + 1 ) ) ∈ ℝ )
23 4 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ - 𝑁 ∈ ℤ ) → ( 𝐴 Yrm - 𝑁 ) ∈ ℤ )
24 1 18 23 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm - 𝑁 ) ∈ ℤ )
25 24 zred ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm - 𝑁 ) ∈ ℝ )
26 rmy0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
27 26 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm 0 ) = 0 )
28 simpr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 𝑁 ≤ 0 )
29 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
30 29 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 𝑁 ∈ ℝ )
31 30 le0neg1d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝑁 ≤ 0 ↔ 0 ≤ - 𝑁 ) )
32 28 31 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 ≤ - 𝑁 )
33 0zd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 ∈ ℤ )
34 zleltp1 ⊢ ( ( 0 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( 0 ≤ - 𝑁 ↔ 0 < ( - 𝑁 + 1 ) ) )
35 33 18 34 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 0 ≤ - 𝑁 ↔ 0 < ( - 𝑁 + 1 ) ) )
36 32 35 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 < ( - 𝑁 + 1 ) )
37 ltrmy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ ( - 𝑁 + 1 ) ∈ ℤ ) → ( 0 < ( - 𝑁 + 1 ) ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm ( - 𝑁 + 1 ) ) ) )
38 1 33 19 37 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 0 < ( - 𝑁 + 1 ) ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm ( - 𝑁 + 1 ) ) ) )
39 36 38 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm ( - 𝑁 + 1 ) ) )
40 27 39 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 < ( 𝐴 Yrm ( - 𝑁 + 1 ) ) )
41 lermy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( 0 ≤ - 𝑁 ↔ ( 𝐴 Yrm 0 ) ≤ ( 𝐴 Yrm - 𝑁 ) ) )
42 1 33 18 41 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 0 ≤ - 𝑁 ↔ ( 𝐴 Yrm 0 ) ≤ ( 𝐴 Yrm - 𝑁 ) ) )
43 32 42 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm 0 ) ≤ ( 𝐴 Yrm - 𝑁 ) )
44 27 43 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 ≤ ( 𝐴 Yrm - 𝑁 ) )
45 22 25 40 44 addgtge0d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 < ( ( 𝐴 Yrm ( - 𝑁 + 1 ) ) + ( 𝐴 Yrm - 𝑁 ) ) )
46 7 recnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℂ )
47 10 recnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
48 46 47 negdid ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → - ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) = ( - ( 𝐴 Yrm ( 𝑁 − 1 ) ) + - ( 𝐴 Yrm 𝑁 ) ) )
49 rmyneg ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm - ( 𝑁 − 1 ) ) = - ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
50 1 3 49 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm - ( 𝑁 − 1 ) ) = - ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
51 rmyneg ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm - 𝑁 ) = - ( 𝐴 Yrm 𝑁 ) )
52 51 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm - 𝑁 ) = - ( 𝐴 Yrm 𝑁 ) )
53 50 52 oveq12d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( ( 𝐴 Yrm - ( 𝑁 − 1 ) ) + ( 𝐴 Yrm - 𝑁 ) ) = ( - ( 𝐴 Yrm ( 𝑁 − 1 ) ) + - ( 𝐴 Yrm 𝑁 ) ) )
54 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
55 54 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 𝑁 ∈ ℂ )
56 ax-1cn ⊢ 1 ∈ ℂ
57 negsubdi ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 𝑁 − 1 ) = ( - 𝑁 + 1 ) )
58 55 56 57 sylancl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → - ( 𝑁 − 1 ) = ( - 𝑁 + 1 ) )
59 58 oveq2d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( 𝐴 Yrm - ( 𝑁 − 1 ) ) = ( 𝐴 Yrm ( - 𝑁 + 1 ) ) )
60 59 oveq1d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( ( 𝐴 Yrm - ( 𝑁 − 1 ) ) + ( 𝐴 Yrm - 𝑁 ) ) = ( ( 𝐴 Yrm ( - 𝑁 + 1 ) ) + ( 𝐴 Yrm - 𝑁 ) ) )
61 48 53 60 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → - ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) = ( ( 𝐴 Yrm ( - 𝑁 + 1 ) ) + ( 𝐴 Yrm - 𝑁 ) ) )
62 45 61 breqtrrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 < - ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) )
63 11 lt0neg1d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < 0 ↔ 0 < - ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
64 62 63 mpbird ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < 0 )
65 15 nn0ge0d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → 0 ≤ ( 𝐴 Xrm 𝑁 ) )
66 11 12 16 64 65 ltletrd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≤ 0 ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )
67 simpll ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 0 < 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
68 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
69 68 biimpri ⊢ ( ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) → 𝑁 ∈ ℕ )
70 69 adantll ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 0 < 𝑁 ) → 𝑁 ∈ ℕ )
71 jm2.24nn ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )
72 67 70 71 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ 0 < 𝑁 ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )
73 29 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
74 0re ⊢ 0 ∈ ℝ
75 lelttric ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑁 ≤ 0 ∨ 0 < 𝑁 ) )
76 73 74 75 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 0 ∨ 0 < 𝑁 ) )
77 66 72 76 mpjaodan ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )