Metamath Proof Explorer

Theorem hashscontpow1

Description: Helper lemma for to prove inequality in Zr. (Contributed by metakunt, 28-Apr-2025)

Ref Expression
Hypotheses hashscontpow1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
hashscontpow1.2 ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
hashscontpow1.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
hashscontpow1.4 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
hashscontpow1.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
hashscontpow1.6 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
hashscontpow1.7 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
hashscontpow1.8 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion hashscontpow1 ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hashscontpow1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 hashscontpow1.2 ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
3 hashscontpow1.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
4 hashscontpow1.4 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
5 hashscontpow1.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
6 hashscontpow1.6 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
7 hashscontpow1.7 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
8 hashscontpow1.8 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
9 3 elfzelzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
10 9 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
11 2 elfzelzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
12 11 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
13 10 12 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
14 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
15 odzcl ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
16 4 14 5 15 syl3anc ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
17 16 nnred ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℝ )
18 elfznn ⊢ ( 𝐴 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝐴 ∈ ℕ )
19 2 18 syl ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
20 19 nnrpd ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
21 10 20 ltsubrpd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) < 𝐵 )
22 elfzle2 ⊢ ( 𝐵 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝐵 ≤ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
23 3 22 syl ⊢ ( 𝜑 → 𝐵 ≤ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
24 13 10 17 21 23 ltletrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
26 odzval ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) = inf ( { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } , ℝ , < ) )
27 4 14 5 26 syl3anc ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) = inf ( { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } , ℝ , < ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) = inf ( { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } , ℝ , < ) )
29 elrabi ⊢ ( 𝑗 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } → 𝑗 ∈ ℕ )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ) → 𝑗 ∈ ℕ )
31 30 nnred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ) → 𝑗 ∈ ℝ )
32 31 ex ⊢ ( 𝜑 → ( 𝑗 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } → 𝑗 ∈ ℝ ) )
33 32 ssrdv ⊢ ( 𝜑 → { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ⊆ ℝ )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ⊆ ℝ )
35 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → 𝑥 = 1 )
37 36 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( 𝑥 ≤ 𝑦 ↔ 1 ≤ 𝑦 ) )
38 37 ralbidv ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ∀ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } 1 ≤ 𝑦 ) )
39 elrabi ⊢ ( 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } → 𝑦 ∈ ℕ )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ) → 𝑦 ∈ ℕ )
41 40 nnge1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ) → 1 ≤ 𝑦 )
42 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } 1 ≤ 𝑦 )
43 35 38 42 rspcedvd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } 𝑥 ≤ 𝑦 )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } 𝑥 ≤ 𝑦 )
45 oveq2 ⊢ ( 𝑖 = ( 𝐵 − 𝐴 ) → ( 𝑁 ↑ 𝑖 ) = ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) )
46 45 oveq1d ⊢ ( 𝑖 = ( 𝐵 − 𝐴 ) → ( ( 𝑁 ↑ 𝑖 ) − 1 ) = ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) )
47 46 breq2d ⊢ ( 𝑖 = ( 𝐵 − 𝐴 ) → ( 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) ↔ 𝑅 ∥ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) )
48 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝐵 ∈ ℤ )
49 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝐴 ∈ ℤ )
50 48 49 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
51 12 10 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
52 8 51 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 0 < ( 𝐵 − 𝐴 ) )
54 50 53 jca ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( 𝐵 − 𝐴 ) ∈ ℤ ∧ 0 < ( 𝐵 − 𝐴 ) ) )
55 elnnz ⊢ ( ( 𝐵 − 𝐴 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) ∈ ℤ ∧ 0 < ( 𝐵 − 𝐴 ) ) )
56 54 55 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℕ )
57 4 nnzd ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
58 57 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝑅 ∈ ℤ )
59 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝑁 ∈ ℤ )
60 19 nnnn0d ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝐴 ∈ ℕ0 )
62 59 61 zexpcld ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝑁 ↑ 𝐴 ) ∈ ℤ )
63 56 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℕ0 )
64 59 63 zexpcld ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ∈ ℤ )
65 1zzd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 1 ∈ ℤ )
66 64 65 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ∈ ℤ )
67 58 62 66 3jca ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝑅 ∈ ℤ ∧ ( 𝑁 ↑ 𝐴 ) ∈ ℤ ∧ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ∈ ℤ ) )
68 simpr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) )
69 68 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) )
70 4 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
71 70 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝑅 ∈ ℕ0 )
72 elfznn ⊢ ( 𝐵 ∈ ( 1 ... ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝐵 ∈ ℕ )
73 3 72 syl ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
74 73 nnnn0d ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
75 14 74 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐵 ) ∈ ℤ )
76 75 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝑁 ↑ 𝐵 ) ∈ ℤ )
77 7 6 zndvds ⊢ ( ( 𝑅 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐵 ) ∈ ℤ ∧ ( 𝑁 ↑ 𝐴 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) ↔ 𝑅 ∥ ( ( 𝑁 ↑ 𝐵 ) − ( 𝑁 ↑ 𝐴 ) ) ) )
78 71 76 62 77 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) ↔ 𝑅 ∥ ( ( 𝑁 ↑ 𝐵 ) − ( 𝑁 ↑ 𝐴 ) ) ) )
79 69 78 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ 𝐵 ) − ( 𝑁 ↑ 𝐴 ) ) )
80 14 60 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐴 ) ∈ ℤ )
81 80 zcnd ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐴 ) ∈ ℂ )
82 9 11 zsubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℤ )
83 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
84 83 13 52 ltled ⊢ ( 𝜑 → 0 ≤ ( 𝐵 − 𝐴 ) )
85 82 84 jca ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) ∈ ℤ ∧ 0 ≤ ( 𝐵 − 𝐴 ) ) )
86 elnn0z ⊢ ( ( 𝐵 − 𝐴 ) ∈ ℕ0 ↔ ( ( 𝐵 − 𝐴 ) ∈ ℤ ∧ 0 ≤ ( 𝐵 − 𝐴 ) ) )
87 85 86 sylibr ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℕ0 )
88 14 87 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ∈ ℤ )
89 88 zcnd ⊢ ( 𝜑 → ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ∈ ℂ )
90 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
91 81 89 90 subdid ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) = ( ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ) − ( ( 𝑁 ↑ 𝐴 ) · 1 ) ) )
92 12 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
93 10 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
94 92 93 pncan3d ⊢ ( 𝜑 → ( 𝐴 + ( 𝐵 − 𝐴 ) ) = 𝐵 )
95 94 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝐴 + ( 𝐵 − 𝐴 ) ) )
96 95 oveq2d ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐵 ) = ( 𝑁 ↑ ( 𝐴 + ( 𝐵 − 𝐴 ) ) ) )
97 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
98 97 87 60 expaddd ⊢ ( 𝜑 → ( 𝑁 ↑ ( 𝐴 + ( 𝐵 − 𝐴 ) ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ) )
99 96 98 eqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐵 ) = ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ) )
100 99 eqcomd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ) = ( 𝑁 ↑ 𝐵 ) )
101 81 mulridd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐴 ) · 1 ) = ( 𝑁 ↑ 𝐴 ) )
102 100 101 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 𝐴 ) · ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) ) − ( ( 𝑁 ↑ 𝐴 ) · 1 ) ) = ( ( 𝑁 ↑ 𝐵 ) − ( 𝑁 ↑ 𝐴 ) ) )
103 91 102 eqtr2d ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐵 ) − ( 𝑁 ↑ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( 𝑁 ↑ 𝐵 ) − ( 𝑁 ↑ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) )
105 79 104 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) )
106 57 80 gcdcomd ⊢ ( 𝜑 → ( 𝑅 gcd ( 𝑁 ↑ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐴 ) gcd 𝑅 ) )
107 rpexp ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( ( ( 𝑁 ↑ 𝐴 ) gcd 𝑅 ) = 1 ↔ ( 𝑁 gcd 𝑅 ) = 1 ) )
108 14 57 19 107 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 𝐴 ) gcd 𝑅 ) = 1 ↔ ( 𝑁 gcd 𝑅 ) = 1 ) )
109 5 108 mpbird ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐴 ) gcd 𝑅 ) = 1 )
110 106 109 eqtrd ⊢ ( 𝜑 → ( 𝑅 gcd ( 𝑁 ↑ 𝐴 ) ) = 1 )
111 110 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝑅 gcd ( 𝑁 ↑ 𝐴 ) ) = 1 )
112 105 111 jca ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝑅 ∥ ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) ∧ ( 𝑅 gcd ( 𝑁 ↑ 𝐴 ) ) = 1 ) )
113 coprmdvds ⊢ ( ( 𝑅 ∈ ℤ ∧ ( 𝑁 ↑ 𝐴 ) ∈ ℤ ∧ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ∈ ℤ ) → ( ( 𝑅 ∥ ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) ∧ ( 𝑅 gcd ( 𝑁 ↑ 𝐴 ) ) = 1 ) → 𝑅 ∥ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) )
114 113 imp ⊢ ( ( ( 𝑅 ∈ ℤ ∧ ( 𝑁 ↑ 𝐴 ) ∈ ℤ ∧ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ∈ ℤ ) ∧ ( 𝑅 ∥ ( ( 𝑁 ↑ 𝐴 ) · ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) ) ∧ ( 𝑅 gcd ( 𝑁 ↑ 𝐴 ) ) = 1 ) ) → 𝑅 ∥ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) )
115 67 112 114 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ ( 𝐵 − 𝐴 ) ) − 1 ) )
116 47 56 115 elrabd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } )
117 infrelb ⊢ ( ( { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } 𝑥 ≤ 𝑦 ∧ ( 𝐵 − 𝐴 ) ∈ { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } ) → inf ( { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } , ℝ , < ) ≤ ( 𝐵 − 𝐴 ) )
118 34 44 116 117 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → inf ( { 𝑖 ∈ ℕ ∣ 𝑅 ∥ ( ( 𝑁 ↑ 𝑖 ) − 1 ) } , ℝ , < ) ≤ ( 𝐵 − 𝐴 ) )
119 28 118 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( 𝐵 − 𝐴 ) )
120 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
121 120 nnred ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℝ )
122 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
123 121 122 lenltd ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( 𝐵 − 𝐴 ) ↔ ¬ ( 𝐵 − 𝐴 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
124 119 123 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) ) → ¬ ( 𝐵 − 𝐴 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
125 25 124 pm2.65da ⊢ ( 𝜑 → ¬ ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) = ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) )
126 125 neqned ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑁 ↑ 𝐴 ) ) ≠ ( 𝐿 ‘ ( 𝑁 ↑ 𝐵 ) ) )