Metamath Proof Explorer

Theorem oexpreposd

Description: Lemma for dffltz . (Contributed by Steven Nguyen, 4-Mar-2023)

Ref Expression
Hypotheses oexpreposd.n ⊢ φ → N ∈ ℝ
oexpreposd.m ⊢ φ → M ∈ ℕ
oexpreposd.1 ⊢ φ → ¬ M 2 ∈ ℕ
Assertion oexpreposd ⊢ φ → 0 < N ↔ 0 < N M

Proof

Step Hyp Ref Expression
1 oexpreposd.n ⊢ φ → N ∈ ℝ
2 oexpreposd.m ⊢ φ → M ∈ ℕ
3 oexpreposd.1 ⊢ φ → ¬ M 2 ∈ ℕ
4 1 adantr ⊢ φ ∧ 0 < N → N ∈ ℝ
5 2 nnzd ⊢ φ → M ∈ ℤ
6 5 adantr ⊢ φ ∧ 0 < N → M ∈ ℤ
7 simpr ⊢ φ ∧ 0 < N → 0 < N
8 expgt0 ⊢ N ∈ ℝ ∧ M ∈ ℤ ∧ 0 < N → 0 < N M
9 4 6 7 8 syl3anc ⊢ φ ∧ 0 < N → 0 < N M
10 9 ex ⊢ φ → 0 < N → 0 < N M
11 0red ⊢ φ → 0 ∈ ℝ
12 11 1 lttrid ⊢ φ → 0 < N ↔ ¬ 0 = N ∨ N < 0
13 12 notbid ⊢ φ → ¬ 0 < N ↔ ¬ ¬ 0 = N ∨ N < 0
14 notnotr ⊢ ¬ ¬ 0 = N ∨ N < 0 → 0 = N ∨ N < 0
15 0re ⊢ 0 ∈ ℝ
16 15 ltnri ⊢ ¬ 0 < 0
17 2 0expd ⊢ φ → 0 M = 0
18 17 breq2d ⊢ φ → 0 < 0 M ↔ 0 < 0
19 16 18 mtbiri ⊢ φ → ¬ 0 < 0 M
20 19 adantr ⊢ φ ∧ 0 = N → ¬ 0 < 0 M
21 simpr ⊢ φ ∧ 0 = N → 0 = N
22 21 eqcomd ⊢ φ ∧ 0 = N → N = 0
23 22 oveq1d ⊢ φ ∧ 0 = N → N M = 0 M
24 23 breq2d ⊢ φ ∧ 0 = N → 0 < N M ↔ 0 < 0 M
25 20 24 mtbird ⊢ φ ∧ 0 = N → ¬ 0 < N M
26 25 ex ⊢ φ → 0 = N → ¬ 0 < N M
27 1 renegcld ⊢ φ → − N ∈ ℝ
28 27 adantr ⊢ φ ∧ 0 < − N → − N ∈ ℝ
29 5 adantr ⊢ φ ∧ 0 < − N → M ∈ ℤ
30 simpr ⊢ φ ∧ 0 < − N → 0 < − N
31 expgt0 ⊢ − N ∈ ℝ ∧ M ∈ ℤ ∧ 0 < − N → 0 < − N M
32 28 29 30 31 syl3anc ⊢ φ ∧ 0 < − N → 0 < − N M
33 32 ex ⊢ φ → 0 < − N → 0 < − N M
34 1 recnd ⊢ φ → N ∈ ℂ
35 simpr ⊢ φ ∧ M 2 ∈ ℤ → M 2 ∈ ℤ
36 zq ⊢ M 2 ∈ ℤ → M 2 ∈ ℚ
37 36 adantl ⊢ φ ∧ M 2 ∈ ℤ → M 2 ∈ ℚ
38 qden1elz ⊢ M 2 ∈ ℚ → denom ⁡ M 2 = 1 ↔ M 2 ∈ ℤ
39 37 38 syl ⊢ φ ∧ M 2 ∈ ℤ → denom ⁡ M 2 = 1 ↔ M 2 ∈ ℤ
40 35 39 mpbird ⊢ φ ∧ M 2 ∈ ℤ → denom ⁡ M 2 = 1
41 40 oveq2d ⊢ φ ∧ M 2 ∈ ℤ → M 2 ⁢ denom ⁡ M 2 = M 2 ⋅ 1
42 qmuldeneqnum ⊢ M 2 ∈ ℚ → M 2 ⁢ denom ⁡ M 2 = numer ⁡ M 2
43 37 42 syl ⊢ φ ∧ M 2 ∈ ℤ → M 2 ⁢ denom ⁡ M 2 = numer ⁡ M 2
44 35 zcnd ⊢ φ ∧ M 2 ∈ ℤ → M 2 ∈ ℂ
45 44 mulid1d ⊢ φ ∧ M 2 ∈ ℤ → M 2 ⋅ 1 = M 2
46 41 43 45 3eqtr3rd ⊢ φ ∧ M 2 ∈ ℤ → M 2 = numer ⁡ M 2
47 2 nnred ⊢ φ → M ∈ ℝ
48 2re ⊢ 2 ∈ ℝ
49 48 a1i ⊢ φ → 2 ∈ ℝ
50 2 nngt0d ⊢ φ → 0 < M
51 2pos ⊢ 0 < 2
52 51 a1i ⊢ φ → 0 < 2
53 47 49 50 52 divgt0d ⊢ φ → 0 < M 2
54 qgt0numnn ⊢ M 2 ∈ ℚ ∧ 0 < M 2 → numer ⁡ M 2 ∈ ℕ
55 36 53 54 syl2anr ⊢ φ ∧ M 2 ∈ ℤ → numer ⁡ M 2 ∈ ℕ
56 46 55 eqeltrd ⊢ φ ∧ M 2 ∈ ℤ → M 2 ∈ ℕ
57 3 56 mtand ⊢ φ → ¬ M 2 ∈ ℤ
58 evend2 ⊢ M ∈ ℤ → 2 ∥ M ↔ M 2 ∈ ℤ
59 5 58 syl ⊢ φ → 2 ∥ M ↔ M 2 ∈ ℤ
60 57 59 mtbird ⊢ φ → ¬ 2 ∥ M
61 oexpneg ⊢ N ∈ ℂ ∧ M ∈ ℕ ∧ ¬ 2 ∥ M → − N M = − N M
62 34 2 60 61 syl3anc ⊢ φ → − N M = − N M
63 62 breq2d ⊢ φ → 0 < − N M ↔ 0 < − N M
64 63 biimpd ⊢ φ → 0 < − N M → 0 < − N M
65 2 nnnn0d ⊢ φ → M ∈ ℕ 0
66 1 65 reexpcld ⊢ φ → N M ∈ ℝ
67 66 renegcld ⊢ φ → − N M ∈ ℝ
68 11 67 lttrid ⊢ φ → 0 < − N M ↔ ¬ 0 = − N M ∨ − N M < 0
69 pm2.46 ⊢ ¬ 0 = − N M ∨ − N M < 0 → ¬ − N M < 0
70 68 69 syl6bi ⊢ φ → 0 < − N M → ¬ − N M < 0
71 33 64 70 3syld ⊢ φ → 0 < − N → ¬ − N M < 0
72 1 lt0neg1d ⊢ φ → N < 0 ↔ 0 < − N
73 66 lt0neg2d ⊢ φ → 0 < N M ↔ − N M < 0
74 73 notbid ⊢ φ → ¬ 0 < N M ↔ ¬ − N M < 0
75 71 72 74 3imtr4d ⊢ φ → N < 0 → ¬ 0 < N M
76 26 75 jaod ⊢ φ → 0 = N ∨ N < 0 → ¬ 0 < N M
77 14 76 syl5 ⊢ φ → ¬ ¬ 0 = N ∨ N < 0 → ¬ 0 < N M
78 13 77 sylbid ⊢ φ → ¬ 0 < N → ¬ 0 < N M
79 10 78 impcon4bid ⊢ φ → 0 < N ↔ 0 < N M