Metamath Proof Explorer

Theorem efchtdvds

Description: The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion efchtdvds ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐴 ) ) ∥ ( exp ‘ ( θ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 chtcl ⊢ ( 𝐵 ∈ ℝ → ( θ ‘ 𝐵 ) ∈ ℝ )
2 1 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐵 ) ∈ ℝ )
3 2 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐵 ) ∈ ℂ )
4 chtcl ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ∈ ℝ )
5 4 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐴 ) ∈ ℝ )
6 5 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ 𝐴 ) ∈ ℂ )
7 efsub ⊢ ( ( ( θ ‘ 𝐵 ) ∈ ℂ ∧ ( θ ‘ 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) = ( ( exp ‘ ( θ ‘ 𝐵 ) ) / ( exp ‘ ( θ ‘ 𝐴 ) ) ) )
8 3 6 7 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) = ( ( exp ‘ ( θ ‘ 𝐵 ) ) / ( exp ‘ ( θ ‘ 𝐴 ) ) ) )
9 chtfl ⊢ ( 𝐵 ∈ ℝ → ( θ ‘ ( ⌊ ‘ 𝐵 ) ) = ( θ ‘ 𝐵 ) )
10 9 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ ( ⌊ ‘ 𝐵 ) ) = ( θ ‘ 𝐵 ) )
11 chtfl ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ ( ⌊ ‘ 𝐴 ) ) = ( θ ‘ 𝐴 ) )
12 11 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( θ ‘ ( ⌊ ‘ 𝐴 ) ) = ( θ ‘ 𝐴 ) )
13 10 12 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( θ ‘ ( ⌊ ‘ 𝐵 ) ) − ( θ ‘ ( ⌊ ‘ 𝐴 ) ) ) = ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) )
14 flword2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) )
15 chtdif ⊢ ( ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) → ( ( θ ‘ ( ⌊ ‘ 𝐵 ) ) − ( θ ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
16 14 15 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( θ ‘ ( ⌊ ‘ 𝐵 ) ) − ( θ ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
17 13 16 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) = Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
18 ssrab2 ⊢ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℝ
19 ax-resscn ⊢ ℝ ⊆ ℂ
20 18 19 sstri ⊢ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℂ
21 20 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℂ )
22 fveq2 ⊢ ( 𝑥 = 𝑦 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) )
23 22 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝑦 ) ∈ ℕ ) )
24 23 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) )
25 fveq2 ⊢ ( 𝑥 = 𝑧 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑧 ) )
26 25 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝑧 ) ∈ ℕ ) )
27 26 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) )
28 fveq2 ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( 𝑦 + 𝑧 ) ) )
29 28 eleq1d ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ ( 𝑦 + 𝑧 ) ) ∈ ℕ ) )
30 simpll ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑦 ∈ ℝ )
31 simprl ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑧 ∈ ℝ )
32 30 31 readdcld ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
33 30 recnd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑦 ∈ ℂ )
34 31 recnd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑧 ∈ ℂ )
35 efadd ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) = ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) )
36 33 34 35 syl2anc ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) = ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) )
37 nnmulcl ⊢ ( ( ( exp ‘ 𝑦 ) ∈ ℕ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) → ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) ∈ ℕ )
38 37 ad2ant2l ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) ∈ ℕ )
39 36 38 eqeltrd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) ∈ ℕ )
40 29 32 39 elrabd ⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
41 24 27 40 syl2anb ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ∧ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
42 41 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ∧ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ) ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
43 fzfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∈ Fin )
44 inss1 ⊢ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ⊆ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) )
45 ssfi ⊢ ( ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∈ Fin ∧ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ⊆ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ) → ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ∈ Fin )
46 43 44 45 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ∈ Fin )
47 fveq2 ⊢ ( 𝑥 = ( log ‘ 𝑝 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( log ‘ 𝑝 ) ) )
48 47 eleq1d ⊢ ( 𝑥 = ( log ‘ 𝑝 ) → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ ( log ‘ 𝑝 ) ) ∈ ℕ ) )
49 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) )
50 49 elin2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
51 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
52 50 51 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
53 52 nnrpd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
54 53 relogcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
55 53 reeflogd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) = 𝑝 )
56 55 52 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) ∈ ℕ )
57 48 54 56 elrabd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
58 0re ⊢ 0 ∈ ℝ
59 1nn ⊢ 1 ∈ ℕ
60 fveq2 ⊢ ( 𝑥 = 0 → ( exp ‘ 𝑥 ) = ( exp ‘ 0 ) )
61 ef0 ⊢ ( exp ‘ 0 ) = 1
62 60 61 eqtrdi ⊢ ( 𝑥 = 0 → ( exp ‘ 𝑥 ) = 1 )
63 62 eleq1d ⊢ ( 𝑥 = 0 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ 1 ∈ ℕ ) )
64 63 elrab ⊢ ( 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 0 ∈ ℝ ∧ 1 ∈ ℕ ) )
65 58 59 64 mpbir2an ⊢ 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ }
66 65 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
67 21 42 46 57 66 fsumcllem ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ... ( ⌊ ‘ 𝐵 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
68 17 67 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
69 fveq2 ⊢ ( 𝑥 = ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) )
70 69 eleq1d ⊢ ( 𝑥 = ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) ∈ ℕ ) )
71 70 elrab ⊢ ( ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ∈ ℝ ∧ ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) ∈ ℕ ) )
72 71 simprbi ⊢ ( ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } → ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) ∈ ℕ )
73 68 72 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( ( θ ‘ 𝐵 ) − ( θ ‘ 𝐴 ) ) ) ∈ ℕ )
74 8 73 eqeltrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( exp ‘ ( θ ‘ 𝐵 ) ) / ( exp ‘ ( θ ‘ 𝐴 ) ) ) ∈ ℕ )
75 74 nnzd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( exp ‘ ( θ ‘ 𝐵 ) ) / ( exp ‘ ( θ ‘ 𝐴 ) ) ) ∈ ℤ )
76 efchtcl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( θ ‘ 𝐴 ) ) ∈ ℕ )
77 76 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐴 ) ) ∈ ℕ )
78 77 nnzd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐴 ) ) ∈ ℤ )
79 77 nnne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐴 ) ) ≠ 0 )
80 efchtcl ⊢ ( 𝐵 ∈ ℝ → ( exp ‘ ( θ ‘ 𝐵 ) ) ∈ ℕ )
81 80 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐵 ) ) ∈ ℕ )
82 81 nnzd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐵 ) ) ∈ ℤ )
83 dvdsval2 ⊢ ( ( ( exp ‘ ( θ ‘ 𝐴 ) ) ∈ ℤ ∧ ( exp ‘ ( θ ‘ 𝐴 ) ) ≠ 0 ∧ ( exp ‘ ( θ ‘ 𝐵 ) ) ∈ ℤ ) → ( ( exp ‘ ( θ ‘ 𝐴 ) ) ∥ ( exp ‘ ( θ ‘ 𝐵 ) ) ↔ ( ( exp ‘ ( θ ‘ 𝐵 ) ) / ( exp ‘ ( θ ‘ 𝐴 ) ) ) ∈ ℤ ) )
84 78 79 82 83 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( exp ‘ ( θ ‘ 𝐴 ) ) ∥ ( exp ‘ ( θ ‘ 𝐵 ) ) ↔ ( ( exp ‘ ( θ ‘ 𝐵 ) ) / ( exp ‘ ( θ ‘ 𝐴 ) ) ) ∈ ℤ ) )
85 75 84 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( exp ‘ ( θ ‘ 𝐴 ) ) ∥ ( exp ‘ ( θ ‘ 𝐵 ) ) )